Formal verification techniques usually work for closed homogeneous non-distributed applications. For example, taking Java as an example language and model checking as an example verification method, Java model-checking techniques work for programs that are self-executable, written in pure Java and ready to run on a single Java Virtual Machine (JVM). However, there are many applications that are open, heterogeneous, and distributed in nature, e.g., web applications, which are: 1) driven by an end user; 2) comprised of artifacts written in many languages (e.g., Java, JavaScript, HTML, and XML); and/or 3) deployed in a distributed environment, with client, server, and database potentially residing on different machines. To apply Java model-checking techniques, all non-Java components (including a user) need to be represented as pure Java implementations. In addition, the distributed nature of applications needs to be dealt with so that the resulting Java program is non-distributed but preserves all of the relevant behaviors of the original application. As with all such processing operations, of critical importance are issues relating to speed, accuracy, and automation.